Generate user documentation for varconds and proof script commands - #3977

We might want to discuss whether we want to introduce this library https://github.com/dnault/therapi-runtime-javadoc

Which brings annotations and an annotation processor that writes annotations capturing the Javadoc to Clazz and other Java entities for runtime usage

Current version:

\applyUpdateOnRigid

This variable condition can be used to check whether an update can be performed on a formula or
term.
That is the case if the top-level operator is rigid and of arity greater than 0.

Signatures

• \applyUpdateOnRigid(u: VARIABLE, phi: VARIABLE, result: VARIABLE)

  Creates an instance of the variable condition.

  • u the schema variable matched against an update
  • phi the schema variable matched against a formula or term
  • result the schema variable containing the result of applying u on
    phi

\containsAssignment

This variable condition can be used to check whether an assignment expression occurs as a
subexpression of a schemavariable instantiation,

Signatures

• \containsAssignment(x: VARIABLE)

• \not\containsAssignment(x: VARIABLE)

  creates an instance of the variable condition

  • x the schemavariable whose instantiation is to be checked
  • negated true iff the check should ensure the absence of an assignment statement

\different

A variable condition for the taclet construct \different, ensuring that two schema
variables are instantiated with distinct elements.

Signatures

• \different(var1: VARIABLE, var2: VARIABLE)

  Instantiates a new different-instantiation condition.

  • var1 the first schema variable
  • var2 the second schema variable; both must not be instantiated with the same element

\differentFields

This variable condition checks if given two terms s, t both terms have a different unique symbol
as top level operator

Signatures

• \differentFields(var1: VARIABLE, var2: VARIABLE)

  Instantiates a new different-fields condition.

  • var1 the first schema variable; both instantiations must differ in their top-level
    unique function symbol
  • var2 the second schema variable

\disjointModuloNull

General varcond for checking relationships between types of schema variables.

Signatures

• \disjointModuloNull(: TYPE_RESOLVER, : TYPE_RESOLVER)

\dropEffectlessElementaries

A variable condition for the taclet construct \dropEffectlessElementaries: given an
update and a target term, it computes the update with all elementary updates removed that do not
affect (are not "relevant" for) the target term, and binds the result to a third schema variable.

Signatures

• \dropEffectlessElementaries(u: VARIABLE, x: VARIABLE, x2: VARIABLE)

  Instantiates a new drop-effectless-elementaries condition.

  • u the update schema variable whose instantiation is simplified
  • x the schema variable holding the target term which determines the relevant locations
  • x2 the schema variable to which the simplified update application
    u(x) is bound

\dropEffectlessStores

A variable condition for the taclet construct \dropEffectlessStores: it removes all
store operations from a heap term that are overwritten by later store operations
on the same location, and binds the simplified heap to a result schema variable.

Signatures

• \dropEffectlessStores(h: VARIABLE, o: VARIABLE, f: VARIABLE, x: VARIABLE, result: VARIABLE)

  Instantiates a new drop-effectless-stores condition.

  • h the term schema variable for the heap on which the store operation is performed
  • o the term schema variable for the object of the store operation
  • f the term schema variable for the field of the store operation
  • x the term schema variable for the value written by the store operation
  • result the term schema variable to which the heap with all effectless stores removed
    is bound

\equalUnique

A variable condition for the taclet construct \equalUnique: checks that two term schema
variables are instantiated with (distinct) applications of functions marked as unique,
and if so binds a formula schema variable to the equation of both terms.

Signatures

• \equalUnique(t: VARIABLE, t2: VARIABLE, res: VARIABLE)

  Instantiates a new equal-unique condition.

  • t the first term schema variable; its instantiation must be the application of a
    unique function
  • t2 the second term schema variable; its instantiation must be the application of a
    unique function
  • res the formula schema variable to which the equation t = t2 is bound

\fieldType

Variable condition that enforces a given generic sort to be instantiated with the type of a field
constant.

The condition can only be fulfilled if the given field term is constant of which the referred
type is known.

Signatures

• \fieldType(exprOrTypeSV: VARIABLE, sort: SORT)

  Instantiates a new field-type condition.

  • exprOrTypeSV the expression or type schema variable whose instantiation must be a
    field constant
  • sort the generic sort which is instantiated with the referred type of the field

\final

ensures that the given instantiation for the schema variable denotes a final field

Signatures

• \final(arg0: VARIABLE)

• \not\final(arg0: VARIABLE)

  the static reference condition checks if a suggested instantiation for a schema variable
  denotes a static reference. The flag negation allows to reuse this condition for ensuring non
  static references.

\freeLabelIn

A variable condition for the taclet construct \freeLabelIn, checking whether a program
label occurs freely in a Java program (block).

Signatures

• \freeLabelIn(label: VARIABLE, statement: VARIABLE)

• \not\freeLabelIn(label: VARIABLE, statement: VARIABLE)

  Instantiates a new free-label-in condition.

  • label the schema variable which must be instantiated with a program label
  • statement the schema variable which must be instantiated with a program element
    (statement)
  • negated whether the condition is negated (\not freeLabelIn)

\getFreeInvariant

Extracts the free loop invariants for the given loop term. Free invariants are only assumed, but
not proven (like an axiom).

Signatures

• \getFreeInvariant(loopStmtSV: VARIABLE, modalitySV: VARIABLE, invSV: VARIABLE)

  Instantiates a new free-loop-invariant condition.

  • loopStmtSV the program schema variable which must be instantiated with a loop
    statement
  • modalitySV the schema variable for the modality kind determining the applicable heap
    context
  • invSV the schema variable to which the free loop invariant is bound

\getInvariant

Extracts the loop invariants for a loop term (for all applicable heap contexts).

Signatures

• \getInvariant(loopStmtSV: VARIABLE, modalitySV: VARIABLE, invSV: VARIABLE)

  Instantiates a new loop-invariant condition.

  • loopStmtSV the program schema variable which must be instantiated with a loop
    statement
  • modalitySV the schema variable for the modality kind determining the applicable heap
    context
  • invSV the schema variable to which the loop invariant is bound

\getVariant

Extracts the variant for a loop term.

Signatures

• \getVariant(loopStmtSV: VARIABLE, variantSV: VARIABLE)

  Instantiates a new loop-variant condition.

  • loopStmtSV the program schema variable which must be instantiated with a loop
    statement
  • variantSV the schema variable to which the loop variant is bound

\hasElementarySort

Variable condition that enforces a given generic sort to be instantiated with the sort of a
program expression a schema variable is instantiated with

Signatures

• \hasElementarySort(: VARIABLE, : SORT)

\hasInvariant

Checks whether a loop has an invariant (either normal or "free").

Signatures

• \hasInvariant(loopStmtSV: VARIABLE, modalitySV: VARIABLE)

  Instantiates a new has-loop-invariant condition.

  • loopStmtSV the program schema variable which must be instantiated with a loop
    statement
  • modalitySV the schema variable for the modality kind determining the applicable heap
    context

\hasLabel

This variable condition checks if an instantiation for term labels contains a specific term
label.

Signatures

• \hasLabel(l: VARIABLE, t: STRING)

• \not\hasLabel(l: VARIABLE, t: STRING)

  Instantiates a new term-label condition.

  • l the term-label schema variable whose instantiations are searched for the label
  • t the name of the term label to look for
  • negated whether the condition is negated (\not hasLabel)

\hasSort

Variable condition that enforces a given generic sort to be instantiated with the sort of a
program expression a schema variable is instantiated with

Signatures

• \hasSort(: VARIABLE, : SORT)

\hasSubFormulas

This variable condition checks if an instantiation for a formula has sub formulas which are
formulas. It returns false for an arity equal to zero or no sub formulas. This is needed to
simplify distinguishing between different well-definedness operators in taclets, since the
difference exists only for formulas.

Signatures

• \hasSubFormulas(a: VARIABLE)

• \not\hasSubFormulas(a: VARIABLE)

  Instantiates a new sub-formula condition.

  • a the formula schema variable whose instantiation is checked for formula sub-terms
  • negated whether the condition is negated (\not hasSubFormulas)

\isAbstractOrInterface

This variable condition checks if a given type denotes an abstract class or interface type.

Signatures

• \isAbstractOrInterface(tr: TYPE_RESOLVER)

• \not\isAbstractOrInterface(tr: TYPE_RESOLVER)

  Instantiates a new abstract-or-interface condition.

  • tr the type resolver for the type to check
  • negation whether the condition is negated (\not isAbstractOrInterface)

\isArray

This variable condition checks if an instantiation is an array.

Signatures

• \isArray(var: VARIABLE)

• \not\isArray(var: VARIABLE)

  creates an instance of this condition checking if an instantiation of a schema variable is an
  array or not

  • var the SchemaVariable to be checked
  • negated if the result is to be negated upon finding

\isArrayLength

A variable condition for the taclet construct \isArrayLength, checking that a schema
variable is instantiated with the implicit array length attribute.

Signatures

• \isArrayLength(reference: VARIABLE)

• \not\isArrayLength(reference: VARIABLE)

  Instantiates a new array length condition.

  • reference the schema variable which must be instantiated with the array length
    attribute of some array type
  • negation whether the condition is negated (\not isArrayLength)

\isConstant

This variable condition checks if an instantiation is a constant formula or term, i.e. its arity
is equal to zero.

Signatures

• \isConstant(t: VARIABLE)

• \not\isConstant(t: VARIABLE)

  Instantiates a new constant condition.

  • t the term or formula schema variable which must be instantiated with a constant
    (zero-arity) term
  • negated whether the condition is negated (\not isConstant)

\isEnumConst

ensures that the given instantiation for the schemavariable denotes a constant of an enum type.

Signatures

• \isEnumConst(arg0: VARIABLE)

  the static reference condition checks if a suggested instantiation for a schema variable
  denotes a reference to an enum constant.

\isFinal

This variable condition checks if a given type denotes a final type.

Final types are either primitive types or classes that are declared final or arrays of final
types.

Signatures

• \isFinal(tr: TYPE_RESOLVER)

• \not\isFinal(tr: TYPE_RESOLVER)

  Instantiates a new final-type condition.

  • tr the type resolver for the type to check
  • negation whether the condition is negated (\not isFinal)

\isInStrictFp

This variable condition checks if a context is affected by the strictfp modifier

Signatures

• \isInStrictFp()

• \not\isInStrictFp()

  Instantiates a new strict-fp condition.

  • negation whether the condition is negated (\not isInStrictFp)

\isLabeled

Checks whether the given statement is labeled, i.e., actual a LabeledStatement. This information
is obtained from the program prefix.

Signatures

• \isLabeled(stmtSV: VARIABLE)

• \not\isLabeled(stmtSV: VARIABLE)

  Instantiates a new is-labeled condition.

  • stmtSV the program schema variable which must be instantiated with a labeled
    statement
  • negated whether the condition is negated (\not isLabeled)

\isLocalVariable

Ensures the given ProgramElement denotes a local variable

Signatures

• \isLocalVariable(var: VARIABLE)

• \not\isLocalVariable(var: VARIABLE)

  Instantiates a new local-variable condition.

  • var the schema variable which must be instantiated with a local (non-member) program
    variable
  • neg whether the condition is negated (\not isLocalVariable)

\isModelField

This variable condition checks if the instantiation of a schemavariable (of
type Field) refers to a Java field declared as "model".

The negated condition is true if the instantiation refers to an instance
or static or ghost field.

Signatures

• \isModelField(field: VARIABLE)

• \not\isModelField(field: VARIABLE)

  Instantiates a new model-field condition.

  • field the schema variable which must be instantiated with a Java field
  • negated whether the condition is negated (\not isModelField)

\isObserver

A variable condition for the taclet construct \isObserver, checking that a term schema
variable is instantiated with an observer function and that the heap argument of the observer is
the given heap term. If the heap schema variable is not yet instantiated, it is bound to the
observer's heap argument.

Signatures

• \isObserver(obs: VARIABLE, heap: VARIABLE)

  Instantiates a new observer condition.

  • obs the term schema variable which must be instantiated with an observer function
    application (an {@link IObserverFunction IObserverFunction})
  • heap the term schema variable for the heap on which the observer is evaluated; it is
    automatically instantiated with the observer's heap argument if not yet instantiated

\isReference

This variable condition checks if a schemavariable is instantiated with a reference or primitive
type

Signatures

• \isReference(: TYPE_RESOLVER)
• \not\isReference(: TYPE_RESOLVER)

\isReferenceArray

This variable condition checks if an array component is of reference type

Signatures

• \isReferenceArray(var: VARIABLE)

• \not\isReferenceArray(var: VARIABLE)

  creates an instance of this condition checking if array var has reference or primitive
  component type depending on the value of checkReferenceType

  • var the SchemaVariable to be checked
  • checkReferenceType the boolean flag which when is set (true) FIXME weigl:
    this is not true! checkReferenceType is just the negated flag. checks for reference
    otherwise for primitive type

\isStaticField

This variable condition checks if the instantiation of a schemavariable (of type Field) refers to
a Java field declared as "static".

The negated condition is true if the instantiation refers to an instance (non-static) field.

Inspired by FieldTypeToSortCondition FieldTypeToSortCondition.

Signatures

• \isStaticField(field: VARIABLE)

• \not\isStaticField(field: VARIABLE)

  Instantiates a new static-field condition.

  • field the schema variable which must be instantiated with a Java field
  • negated whether the condition is negated (\not isStaticField)

\isThisReference

This variable condition checks if a program variable is instantiated with a this
reference.

Signatures

• \isThisReference(var: VARIABLE)

• \not\isThisReference(var: VARIABLE)

  Instantiates a new this-reference condition.

  • var the program schema variable which must be instantiated with a this
    reference
  • negation whether the condition is negated (\not isThisReference)

\mayExpandMethod

ensures that the given instantiation for the schemavariable denotes a method whose body may be
expanded. For determining the method the callee and the arguments of the method are needed as
arguments.

A method may be inlinded if:

• the method is private, or
• the method is static, or
• the method is final, or
• the receiver class is final, or
• the corresponding taclet option is set to relaxed inlining.

Signatures

• \mayExpandMethod(receiver: VARIABLE, methname: VARIABLE, args: VARIABLE)

• \not\mayExpandMethod(receiver: VARIABLE, methname: VARIABLE, args: VARIABLE)

  Instantiate a new variable condition.

  • receiver program schema var for the receiver, may be null for class-local calls
  • methname non-null program schema var for the methodname
  • args non-null program schema var for the arguments of the call
  • negation true iff the condition is to be negated

• \mayExpandMethod(methodName: VARIABLE, args: VARIABLE)

• \not\mayExpandMethod(methodName: VARIABLE, args: VARIABLE)

  Instantiate a new variable condition for class-local method calls without an explicit
  receiver.

  • methodName non-null program schema var for the methodname
  • args non-null program schema var for the arguments of the call
  • negation true iff the condition is to be negated

\metaDisjoint

A variable condition for the taclet construct \metaDisjoint, checking that the two
instantiations of the given term schema variables denote provably disjoint location sets.

Signatures

• \metaDisjoint(s1: VARIABLE, s2: VARIABLE)

  Instantiates a new meta-disjoint condition.

  • s1 the first term schema variable; its instantiation is interpreted as a location set
  • s2 the second term schema variable; its instantiation is interpreted as a location set

\new

Signatures

• \new(arg0: VARIABLE, arg1: JAVA_TYPE)

• \new(arg0: VARIABLE, arg1: SORT)

\newDependingOn

Signatures

• \newDependingOn(first: VARIABLE, second: VARIABLE)

\newLabel

This variable condition ensures that no other label of the same name exists in the context
program or one of the schemavariable instantiations.

Signatures

• \newLabel(sv: VARIABLE)

  Instantiates a new jump-label condition.

  • sv the program schema variable of sort LABEL which must be instantiated with
    a label not occurring elsewhere in the context program or the schema variable
    instantiations

\newLocalVars

For the loop scope rule, if a local program variable that may be altered by the loop body appears
in the frame condition,
it is necessary to use the value before the loop first executes in the frame condition.


To achieve this, this condition generates (1) the "before" version of each variable that may be
written to by the loop
MiscTools#getLocalOuts(ProgramElement, Services) MiscTools#getLocalOuts(ProgramElement, Services); (2) an update storing the value of each
such PV in its "before" version,
i.e., {...||i_before := i||...``; (3) the reverse of the update, to be applied to the frame condition, i.e., {...||i := i_before||...``.

Signatures

• \newLocalVars(varDeclsSV: VARIABLE, updateBeforeSV: VARIABLE, updateFrameSV: VARIABLE, bodySV: VARIABLE)

  Instantiates a new local-variables condition.

  • varDeclsSV the schema variable to which the variable declarations for the "before"
    versions of the variables written by the loop are bound
  • updateBeforeSV the schema variable to which the update
    {...||i_before := i||...} is bound
  • updateFrameSV the schema variable to which the reverse update
    {...||i := i_before||...} is bound
  • bodySV the schema variable holding the loop body

\newTypeOf

Signatures

• \newTypeOf(arg0: VARIABLE, arg1: VARIABLE)

\notFreeIn

Signatures

• \notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE)

• \not\notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE)

• \notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE)

• \not\notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE)

• \notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE)

• \not\notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE, : VARIABLE)

• \notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE)

• \not\notFreeIn(: VARIABLE, : VARIABLE, : VARIABLE)

• \notFreeIn(: VARIABLE, : VARIABLE)

• \not\notFreeIn(: VARIABLE, : VARIABLE)

\reference

This variable condition checks if a type is an enum type.

Signatures

• \reference(resolver: VARIABLE)

• \not\reference(resolver: VARIABLE)

  creates a condition that checks if a type is a EnumDeclaration

  • resolver the type resolver to be checked
  • negated should the result be negated

\same

General varcond for checking relationships between types of schema variables.

Signatures

• \same(fst: TYPE_RESOLVER, snd: TYPE_RESOLVER)

• \not\same(fst: TYPE_RESOLVER, snd: TYPE_RESOLVER)

  creates a condition that checks if the declaration types of the schemavariable's
  instantiations are unequal

  • fst one of the SchemaVariable whose type is checked
  • snd one of the SchemaVariable whose type is checked
  • mode an int encoding if testing of not same or not compatible

\sameObserver

A variable condition that is satisfied if the two arguments are

• schema variables,
• their instantiations are terms of observer functions,
• with the same function,
• which as exactly one heap argument
• and has got a dependency contract

,

Limitations

Currently, this and de.uka.ilkd.key.rule.metaconstruct.ObserverEqualityMetaConstruct de.uka.ilkd.key.rule.metaconstruct.ObserverEqualityMetaConstruct only
support observers with a single heap argument, that should be generalised.

Signatures

• \sameObserver(schema1: VARIABLE, schema2: VARIABLE)

  Create a new condition

  • schema1 first argument, must be schema variable
  • schema2 2nd argument, must be schema variable

• \sameObserver(schema1: VARIABLE, schema2: VARIABLE)

  Create a new condition

  • schema1 first argument, must be schema variable
  • schema2 2nd argument, must be schema variable

\scrictSub

General varcond for checking relationships between types of schema variables.

Signatures

• \scrictSub(: TYPE_RESOLVER, : TYPE_RESOLVER)

\simplifyIfThenElseUpdate

A variable condition for the taclet construct \simplifyIfThenElseUpdate: it turns two
updates guarded by a condition phi into a single parallel update whose right-hand sides
are if phi then r1 else r2 expressions, and binds the common condition to a formula
schema variable.

Signatures

• \simplifyIfThenElseUpdate(phi: VARIABLE, u1: VARIABLE, u2: VARIABLE, commonFormula: VARIABLE, result: VARIABLE)

  Instantiates a new simplify-if-then-else-update condition.

  • phi the formula schema variable guarding the two updates
  • u1 the update schema variable applied if phi holds
  • u2 the update schema variable applied if phi does not hold
  • commonFormula the formula schema variable to which the guard phi is bound
  • result the schema variable to which the merged update
    if phi then u1 else u2 is bound

• \simplifyIfThenElseUpdate(phi: VARIABLE, u1: VARIABLE, u2: VARIABLE, commonFormula: VARIABLE, result: VARIABLE)

  Instantiates a new simplify-if-then-else-update condition.

  • phi the formula schema variable guarding the two updates
  • u1 the update schema variable applied if phi holds
  • u2 the update schema variable applied if phi does not hold
  • commonFormula the formula schema variable to which the guard phi is bound
  • result the schema variable to which the merged update
    if phi then u1 else u2 is bound

\static

ensures that the given instantiation for the schemavariable denotes a static field

Signatures

• \static(arg0: VARIABLE)

• \not\static(arg0: VARIABLE)

  the static reference condition checks if a suggested instantiation for a schema variable
  denotes a static reference. The flag negation allows to reuse this condition for ensuring non
  static references.

\staticMethodReference

ensures that the given instantiation for the schemavariable denotes a static method. For
determining the method the callee and the arguments of the method are needed as arguments.

Signatures

• \staticMethodReference(arg0: VARIABLE, arg1: VARIABLE, arg2: VARIABLE)

• \not\staticMethodReference(arg0: VARIABLE, arg1: VARIABLE, arg2: VARIABLE)

  the static reference condition checks if a suggested instantiation for a schema variable
  denotes a static method call. The flag negation allows to reuse this condition for ensuring
  non static references.

\storeStmtIn

Stores the given Statement Statement, after substitution of SchemaVariable SchemaVariables, into the given
ProgramSV ProgramSV for later use in other conditions and transformers. The arguments are a
ProgramSV ProgramSV and a JTerm JTerm, where the JTerm JTerm must contain a JavaBlock JavaBlock
with a StatementBlock StatementBlock containing a single statement (that works, e.g., when
passing an expression like
\modality{#allmodal{ while (#e) #body \endmodality(post)); this statement is then
stored (in the example the while statement).

Signatures

• \storeStmtIn(resultVarSV: VARIABLE, term: TERM)

  Instantiates a new store-statement-in condition.

  • resultVarSV the program schema variable to which the extracted statement is bound
  • term the term whose Java block contains the statement to store; the statement is
    substituted with the current schema variable instantiations first

\storeTermIn

Stores the given JTerm JTerm, after substitution of SchemaVariable SchemaVariables, into the given
SchemaVariable SchemaVariable for later use in other conditions and transformers.

Signatures

• \storeTermIn(resultVarSV: VARIABLE, term: TERM)

  Instantiates a new store-term-in condition.

  • resultVarSV the schema variable to which the (substituted) term is bound
  • term the term to store; it is substituted with the current schema variable
    instantiations first

\sub

General varcond for checking relationships between types of schema variables.

Signatures

• \sub(fst: TYPE_RESOLVER, snd: TYPE_RESOLVER)

• \not\sub(fst: TYPE_RESOLVER, snd: TYPE_RESOLVER)

  creates a condition that checks if the declaration types of the schemavariable's
  instantiations are unequal

  • fst one of the SchemaVariable whose type is checked
  • snd one of the SchemaVariable whose type is checked
  • mode an int encoding if testing of not same or not compatible

\subFormulas

This variable condition checks if an instantiation for a formula has sub formulas which are
formulas. It returns false for an arity equal to zero or no sub formulas. This is needed to
simplify distinguishing between different well-definedness operators in taclets, since the
difference exists only for formulas.

Signatures

• \subFormulas(a: VARIABLE)

• \not\subFormulas(a: VARIABLE)

  Instantiates a new sub-formula condition.

  • a the formula schema variable whose instantiation is checked for formula sub-terms
  • negated whether the condition is negated (\not hasSubFormulas)